./smc.sh crowds.prism crowds.props -prop positive -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams S:10000000,Av:10,e:0.001,d:0.05,p:0.05,post:64 -const TotalRuns=6,CrowdSize=20
PRISM-games
===========
Version: 2.0.beta3
Date: Thu Mar 19 11:27:39 UTC 2020
Hostname: 68eec9c801d9
Memory limits: cudd=1g, java(heap)=8.9g
Command line: prism crowds.prism crowds.props -prop positive -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams 'S:10000000;Av:10;e:0.001;d:0.05;p:0.05;post:64' -const 'TotalRuns=6,CrowdSize=20' -javamaxmem 10g
Parsing the model file "crowds.prism"...
Parsing properties file "crowds.props"...
1 property:
(1) "positive": P=? [ F observe0>1 ]
Type: DTMC
Modules: crowds
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
---------------------------------------------------------------------
Model checking: "positive": P=? [ F observe0>1 ]
Model constants: TotalRuns=6,CrowdSize=20
Starting heuristic: RTDP_ADJ
IsMDP false Collapse false break false
ColourParams: S:10000000 Av: 10 eps: 0.001 delta: 0.05 pmin: 0.05
TransDelta: 2.37526000926207E-11
HeuristicSG: Version try0
Grey
======================================
JSON: {"Trials":100000,"Precision":0.9191737490225356,"PartialTransDelta":3.557802189044531E-8,"Value":{"Upper":0.9354539704427147,"Lower":0.01628022142017921},"ActionsOfs0":{"Action0":"[0.016280285897726343;0.9354298528268091]"},"GlobalTimerSecs":473.853,"AvgConf":0.9330424177052558,"StateInfos":{"num00":51572,"num11":1530,"numStates":478848,"num01":424732,"avgDist":0.8885259721675441,"numWorking":1014,"numUnset":0,"numClose":53102}}
JSON: {"Trials":200000,"Precision":0.8686794797655047,"PartialTransDelta":2.564499732779128E-8,"Value":{"Upper":0.8930069624986336,"Lower":0.024327482733128927},"ActionsOfs0":{"Action0":"[0.02432753486644694;0.8929765773054578]"},"GlobalTimerSecs":1058.52,"AvgConf":0.9175946149583049,"StateInfos":{"num00":77917,"num11":2060,"numStates":655654,"num01":567830,"avgDist":0.8773755566661463,"numWorking":7847,"numUnset":0,"numClose":79977}}
JSON: {"Trials":300000,"Precision":0.8283351975989659,"PartialTransDelta":2.1283297719281818E-8,"Value":{"Upper":0.8584654253882354,"Lower":0.030130227789269517},"ActionsOfs0":{"Action0":"[0.03013044317160463;0.8584360887984896]"},"GlobalTimerSecs":1735.894,"AvgConf":0.9133996897347881,"StateInfos":{"num00":104062,"num11":2446,"numStates":780617,"num01":662846,"avgDist":0.862473877604696,"numWorking":11263,"numUnset":0,"numClose":106508}}
----------
Computation aborted after 1800.1794917583466 seconds since the total time limit of 1800 seconds was exceeded.